Require Import List.
Require Import Bool.
Require Import Arith.

Set Implicit Arguments.

Definition swap(A:Type)(a:list A)(i j:nat)(default:A) :=
  (firstn i a) ++ ((nth j a default)::nil) ++ (skipn (i+1) (firstn j a)) ++ 
  ((nth i a default)::nil) ++ (skipn (j+1) a).

Eval compute in swap (1::2::3::4::5::nil) 0 5 100.

Fixpoint two_way_sort(a : list bool)(i len:nat) {struct len}:list bool :=
  match len with
  | 0 => a
  | S len' => 
    if negb(nth i a false) then 
      two_way_sort a (i+1) len'
    else if nth (i+len') a false then
      two_way_sort a i len'
    else
      let a' := swap a i (i+len') false in
        match len' with
        | 0 => a'
        | S len'' => two_way_sort a' (i+1) len''
        end
  end.

Definition drive(a:list bool) := two_way_sort a 0 (length a).    

Eval compute in drive (true::false::false::true::false::nil).    
Eval compute in drive (false::false::true::true::true::nil).    
Eval compute in drive (true::false::false::false::false::nil).    
Eval compute in drive nil.    
      
Theorem ordered : forall(a a':list bool), a' = drive a -> forall(i j:nat), i <= j -> i < length a' -> j < length a' -> Bool.leb (nth i a' false) (nth j a' false).
Proof.
  intros.
